'reach 0.1';



export const main = Reach.App(()=>
  {

   

    const Player = {
      showOwner: Fun([UInt, Address], Null),
      informTimeout: Fun([], Null),
      getTime:Fun([],UInt),
      // getToken:Fun([],Token),
      getAcct:Fun([],Address),
      getInfo:Fun([],Address),
      getRefund:Fun([],Null)
      
    };
  
    const Oracle = Participant('Oracle', {
      ...Player,
      getId: Fun([], UInt),
      get_love: Fun([],UInt),
      get_career: Fun([],UInt),
      get_fortune: Fun([],UInt),
      
    });

    const Buyer = ParticipantClass('Buyer', {
      ...Player,
      buyNFT:Fun([], UInt),
      generat_id:Fun([],UInt),
      showNFT:Fun([],Null),
      pledgeNFT:Fun([],UInt),
      informPledged: Fun([],Null),
      waitPledge:Fun([],Null)
    });

    const OneBuyer = Participant('OneBuyer',
    {
      ...Player,
    }
    )

    const vNFT = View('NFT', {
      id:UInt,
      owner: Address,
      love:UInt,
      career:UInt,
      fortune:UInt
    });

    setOptions({ deployMode: 'constructor'});
    

    deploy();

    


    Anybody.publish();
    const star_token = new Token({name:'star_token                      ', symbol:'SRT     ' ,supply:10000000000000000});
    commit();

    





    

    
  
  //(Oracle, Buyer) => {

    //买NFT，等待打分
    Buyer.only(()=>{
      const Buyer_acc = declassify(interact.getAcct());
      // const star_token = declassify(interact.getToken());
      const generated_time = declassify(interact.buyNFT());
      const generated_id = declassify(interact.generat_id());
      const Buyer_time = declassify(interact.getTime());
    })
    Buyer.publish(Buyer_time,generated_id, generated_time,Buyer_acc).pay(10)
    OneBuyer.set(Buyer_acc);
    commit();


    // const informTimeout = () => {
    //   each([Oracle, Buyer], () => {
    //     interact.informTimeout();
    //   });
    //   // Anybody.publish();
    //   // commit();

    //   // Buyer.only(()=>{
    //   //   interact.getRefund();
    //   // });
    //   // Anybody.publish();
    //   // commit();
    // };

    

    //NFT生成打分
    Oracle.only(() => {
      const time = declassify(interact.getTime());
      const attr_love = declassify(interact.get_love());
      const attr_carrer = declassify(interact.get_career());
      const attr_fortune = declassify(interact.get_fortune());
      const id = declassify(interact.getId());
    });



   

    Oracle.publish(id,time,attr_love,attr_carrer,attr_fortune)
    // .timeout(10,()=>{informTimeout()});

    
    
    
    //铸造NFT
    var NFTowner = Buyer_acc; //var-while
    {
    vNFT.owner.set(Buyer_acc);
    vNFT.love.set(attr_love);
    vNFT.career.set(attr_carrer);
    vNFT.fortune.set(attr_fortune);
    vNFT.id.set(id);
    };
    invariant(NFTowner==Buyer_acc);
    while(true){
    commit();

    //查看或质押NFT
    Buyer.only(()=> {
      interact.showOwner(id,Buyer_acc)
      interact.showNFT()
      
      //质押
      const pledgeTime = declassify(interact.pledgeNFT())
      // const ctc_address = declassify(interact.getInfo());
      //返利
    }) 
    Buyer.publish(pledgeTime);

    vNFT.owner.set(); //持币合约是谁啊????????????????

    commit();

    Buyer.only(() =>{ //等待质押结束
      interact.waitPledge();
      interact.informPledged();
    }
    )
    
    Buyer.publish();
    vNFT.owner.set(this);
    

    //commit();



    // invariant(balance() == 0);
    // transfer(balance()).to(Creator);

    continue;
  }
    
  //}
  star_token.destroy()
  commit();

  assert(false);

  

 
  });

  